/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.test.javasyp.logic;

import static com.googlecode.syper.anno.Pred.ensures;
import static com.googlecode.syper.anno.Pred.exists;
import static com.googlecode.syper.anno.Pred.forall;
import static com.googlecode.syper.anno.Pred.inv;
import static com.googlecode.syper.anno.Pred.requires;

import com.googlecode.syper.anno.BoundsChecks;
import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Result;
import com.googlecode.syper.anno.Pred.IntPred;

import edu.cmu.cs.crystal.annotations.FailingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * Failing tests with forall and exists quantifiers over arrays
 * @author kevin
 * @since May 8, 2010
 * @see QuantifierArrays
 */
@BoundsChecks
@FailingTest(4)
@UseAnalyses("SymbolicChecker")
public class QuantifierArraysFail {

	public void quantifiedTest(final int[] a) {
		requires(0 < a.length & forall(0, a.length, new IntPred() { 
			@Override public boolean cond(int arg) { 
				return 0 <= a[arg];
			}
		}));
		// should fail because pre-condition is too weak (<= vs <)
		assert 0 < a[0];
	}
	
	public int[] quantifiedLoop() {
		int len = 5;
		@Result @Excl final int[] result = new int[len];
		for (int i = 0; i < result.length; i++) {
			// loop invariant should fail
			inv(0 <= i & i <= result.length & result.length == len & 
					forall(0, i, new IntPred() {
						@Override public boolean cond(int arg) { 
							return result[arg] == arg-1;
						}
					}));
			result[i] = i;
		}
		assert result.length == len;
		return result;
	}
	
	public int[] existentialLoop() {
		@Result @Excl final int[] result = new int[5];
//		result[3] = 42; below should fail because no cell has right value
		ensures(exists(0, result.length, new IntPred() {
			@Override public boolean cond(int i) {
				return result[i] == 42;
			}
		}));
		return result;
	}
	
	// TODO need support for mod = "[]"
	// ok right now as summands gets havoced anyway (because assigned in loop)
	public int add(@Excl/*(mod = "[*]")*/ final int[] summands) {
		requires(forall(0, summands.length, new IntPred() {
			@Override public boolean cond(int k) {
				return 0 < summands[k];
			}
		}));
		int result = 0;
		for (int i = 0; i < summands.length; ++i) {
			inv(0 <= i);
			result += summands[i];
			summands[i] = 0;
		}
		// post-condition fails because cells are re-assigned
		// without assignment in array the post-condition should hold
		ensures(forall(0, summands.length, new IntPred() {
			@Override public boolean cond(int k) {
				return 0 < summands[k];
			}
		}));
		return result;
	}

}
